$\forall$$T$, $V$:Type, $A$, $B$:($T$$\rightarrow\mathbb{P}$), ${\it dcd\_A}$:($t$:$T$$\rightarrow$Dec($A$($t$))), $f$:(\{$t$:$T$$\mid$ $A$($t$)\} $\rightarrow$$V$), $g$:(\{$t$:$T$$\mid$ $B$($t$)\} $\rightarrow$$V$).
\\[0ex][$\lambda$$t$.$A$($t$)? $f$ : $g$] $\in$ \{$t$:$T$$\mid$ $A$($t$) $\vee$ $B$($t$)\} $\rightarrow$$V$